$\forall$$i$:Id, ${\it ds}$:$x$:Id fp$\rightarrow$ Type, ${\it da}$:$k$:Knd fp$\rightarrow$ Type, $A$:ecl(${\it ds}$;${\it da}$).
\\[0ex]$\neg$"ecl" $\in$ dom(${\it ds}$) $\Rightarrow$ ecl{-}machine1\{ecl:ut2\}($i$; ${\it ds}$; ${\it da}$; $A$) $\in$ Realizer